the_w:World. FairFifo  (e, e':E. e < e'  time(e)  time(e')) 

latex

Definitions	World, FairFifo, x:AB(x), r  s, e < e', Id, w-info(w;e), P  Q, x.A(x), w-pred(w;e), E, x:A. B(x), t  T, P  Q, P & Q, P  Q, A  B, A, False, Void, a < b, time(e), {x:A| B(x)} ,
Lemmas	nat wf, w-time wf, qle-int, w-E wf, w-pred wf, w-info wf, Id wf, cless wf, fair-fifo wf, world wf, w-cless-decreases